A:Type, eq:EqDecider(A), x,y:A, v:top. (fpf-dom(eq; x; fpf-single(y; v)))  (x = y) 

latex

Definitions	x:A. B(x), t  T, P  Q, b, fpf-dom(eq; x; f), fpf-single(x; v), deq-member(eq; x; L), t.1, reduce(f; k; as), ff, Y, P  Q, P  Q, prop{i:l}, P  Q, if b then t else f fi , P  Q, False
Lemmas	top wf, deq wf, iff functionality wrt iff, assert wf, bor wf, eqof wf, bfalse wf, false wf, assert of bor, or functionality wrt iff, deq property